(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 129))
(declare-fun v1 () (_ BitVec 109))
(declare-fun v2 () (_ BitVec 103))
(declare-fun v3 () (_ BitVec 124))
(assert (let ((e4(_ bv1165271864581375353063059104 91)))
(let ((e5(_ bv185027288818637273614964 78)))
(let ((e6 (bvxnor ((_ sign_extend 51) e5) v0)))
(let ((e7 ((_ extract 52 14) e5)))
(let ((e8 (bvcomp v0 v0)))
(let ((e9 (ite (bvsle ((_ sign_extend 90) e7) e6) (_ bv1 1) (_ bv0 1))))
(let ((e10 (ite (bvsge ((_ zero_extend 6) v2) v1) (_ bv1 1) (_ bv0 1))))
(let ((e11 (concat e5 e8)))
(let ((e12 (ite (= ((_ sign_extend 18) e4) v1) (_ bv1 1) (_ bv0 1))))
(let ((e13 (concat e12 e5)))
(let ((e14 (ite (bvslt ((_ sign_extend 38) e4) e6) (_ bv1 1) (_ bv0 1))))
(let ((e15 ((_ rotate_left 89) e4)))
(let ((e16 (bvudiv e9 e14)))
(let ((e17 (bvcomp ((_ zero_extend 12) e13) e15)))
(let ((e18 (ite (bvsle ((_ sign_extend 108) e10) v1) (_ bv1 1) (_ bv0 1))))
(let ((e19 (concat e17 v1)))
(let ((e20 (bvnor e15 e15)))
(let ((e21 (ite (bvsle ((_ sign_extend 128) e12) e6) (_ bv1 1) (_ bv0 1))))
(let ((e22 (bvand v3 ((_ zero_extend 123) e16))))
(let ((e23 (bvuge ((_ zero_extend 102) e16) v2)))
(let ((e24 (bvslt ((_ zero_extend 123) e21) v3)))
(let ((e25 (bvslt e11 e13)))
(let ((e26 (bvugt e21 e10)))
(let ((e27 (= ((_ zero_extend 128) e16) v0)))
(let ((e28 (bvsle ((_ zero_extend 31) e11) e19)))
(let ((e29 (bvsge v1 ((_ sign_extend 18) e20))))
(let ((e30 (bvule ((_ zero_extend 90) e17) e20)))
(let ((e31 (bvuge e5 ((_ sign_extend 77) e16))))
(let ((e32 (bvuge v3 ((_ sign_extend 33) e20))))
(let ((e33 (bvugt v3 ((_ sign_extend 85) e7))))
(let ((e34 (bvugt v1 ((_ zero_extend 18) e20))))
(let ((e35 (bvult e8 e14)))
(let ((e36 (bvsle ((_ sign_extend 71) e7) e19)))
(let ((e37 (bvsle ((_ sign_extend 40) e7) e13)))
(let ((e38 (bvsge e13 ((_ zero_extend 78) e21))))
(let ((e39 (distinct e6 ((_ zero_extend 90) e7))))
(let ((e40 (= ((_ zero_extend 109) e9) e19)))
(let ((e41 (bvsgt ((_ zero_extend 102) e16) v2)))
(let ((e42 (bvult ((_ sign_extend 90) e9) e20)))
(let ((e43 (distinct e13 ((_ zero_extend 78) e17))))
(let ((e44 (bvsle e9 e16)))
(let ((e45 (= e15 ((_ sign_extend 90) e9))))
(let ((e46 (bvsle ((_ zero_extend 77) e18) e5)))
(let ((e47 (bvult e8 e10)))
(let ((e48 (bvsge e12 e14)))
(let ((e49 (bvult v0 ((_ zero_extend 128) e14))))
(let ((e50 (bvslt ((_ zero_extend 123) e21) v3)))
(let ((e51 (bvslt ((_ zero_extend 33) e15) v3)))
(let ((e52 (bvsgt ((_ sign_extend 18) e20) v1)))
(let ((e53 (bvult v0 ((_ zero_extend 128) e10))))
(let ((e54 (bvsle ((_ zero_extend 38) e8) e7)))
(let ((e55 (bvsle v3 ((_ zero_extend 33) e15))))
(let ((e56 (bvult ((_ zero_extend 77) e12) e5)))
(let ((e57 (bvugt ((_ sign_extend 12) e11) e15)))
(let ((e58 (bvugt ((_ sign_extend 15) v1) v3)))
(let ((e59 (bvule e22 ((_ zero_extend 45) e11))))
(let ((e60 (bvslt ((_ zero_extend 18) e4) v1)))
(let ((e61 (ite e44 e31 e37)))
(let ((e62 (ite e39 e28 e40)))
(let ((e63 (=> e49 e35)))
(let ((e64 (ite e59 e58 e34)))
(let ((e65 (= e36 e51)))
(let ((e66 (ite e41 e65 e23)))
(let ((e67 (=> e60 e48)))
(let ((e68 (xor e47 e47)))
(let ((e69 (not e52)))
(let ((e70 (= e66 e57)))
(let ((e71 (ite e64 e42 e62)))
(let ((e72 (or e71 e71)))
(let ((e73 (=> e29 e53)))
(let ((e74 (not e72)))
(let ((e75 (not e74)))
(let ((e76 (not e63)))
(let ((e77 (or e26 e70)))
(let ((e78 (xor e69 e38)))
(let ((e79 (not e54)))
(let ((e80 (=> e45 e67)))
(let ((e81 (=> e56 e24)))
(let ((e82 (not e33)))
(let ((e83 (and e55 e32)))
(let ((e84 (or e27 e82)))
(let ((e85 (=> e83 e61)))
(let ((e86 (ite e68 e73 e73)))
(let ((e87 (=> e50 e85)))
(let ((e88 (ite e78 e78 e46)))
(let ((e89 (and e25 e79)))
(let ((e90 (xor e77 e84)))
(let ((e91 (= e43 e43)))
(let ((e92 (not e80)))
(let ((e93 (=> e89 e92)))
(let ((e94 (and e93 e87)))
(let ((e95 (not e81)))
(let ((e96 (= e75 e75)))
(let ((e97 (and e91 e76)))
(let ((e98 (=> e30 e88)))
(let ((e99 (or e96 e98)))
(let ((e100 (= e99 e95)))
(let ((e101 (xor e100 e97)))
(let ((e102 (=> e90 e90)))
(let ((e103 (and e102 e101)))
(let ((e104 (= e94 e86)))
(let ((e105 (and e104 e103)))
(let ((e106 (and e105 (not (= e14 (_ bv0 1))))))
e106
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
